'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , top(rec(up(x))) -> top(check(rec(x))) , top(sent(up(x))) -> top(check(rec(x))) , top(no(up(x))) -> top(check(rec(x))) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x)} Details: We have computed the following set of weak (innermost) dependency pairs: { rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(bot()) -> c_3(sent^#(bot())) , rec^#(up(x)) -> c_4(rec^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , no^#(up(x)) -> c_6(no^#(x)) , top^#(rec(up(x))) -> c_7(top^#(check(rec(x)))) , top^#(sent(up(x))) -> c_8(top^#(check(rec(x)))) , top^#(no(up(x))) -> c_9(top^#(check(rec(x)))) , check^#(up(x)) -> c_10(check^#(x)) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(no(x)) -> c_13(no^#(check(x))) , check^#(no(x)) -> c_14(no^#(x))} The usable rules are: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} The estimated dependency graph contains the following edges: {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} ==> {sent^#(up(x)) -> c_5(sent^#(x))} {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} ==> {sent^#(up(x)) -> c_5(sent^#(x))} {rec^#(no(x)) -> c_2(sent^#(rec(x)))} ==> {sent^#(up(x)) -> c_5(sent^#(x))} {rec^#(up(x)) -> c_4(rec^#(x))} ==> {rec^#(up(x)) -> c_4(rec^#(x))} {rec^#(up(x)) -> c_4(rec^#(x))} ==> {rec^#(bot()) -> c_3(sent^#(bot()))} {rec^#(up(x)) -> c_4(rec^#(x))} ==> {rec^#(no(x)) -> c_2(sent^#(rec(x)))} {rec^#(up(x)) -> c_4(rec^#(x))} ==> {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} {rec^#(up(x)) -> c_4(rec^#(x))} ==> {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} {sent^#(up(x)) -> c_5(sent^#(x))} ==> {sent^#(up(x)) -> c_5(sent^#(x))} {no^#(up(x)) -> c_6(no^#(x))} ==> {no^#(up(x)) -> c_6(no^#(x))} {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} ==> {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} ==> {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} ==> {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} ==> {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} ==> {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} ==> {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} ==> {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} ==> {top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} {top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} ==> {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} {check^#(up(x)) -> c_10(check^#(x))} ==> {check^#(no(x)) -> c_14(no^#(x))} {check^#(up(x)) -> c_10(check^#(x))} ==> {check^#(no(x)) -> c_13(no^#(check(x)))} {check^#(up(x)) -> c_10(check^#(x))} ==> {check^#(rec(x)) -> c_12(rec^#(check(x)))} {check^#(up(x)) -> c_10(check^#(x))} ==> {check^#(sent(x)) -> c_11(sent^#(check(x)))} {check^#(up(x)) -> c_10(check^#(x))} ==> {check^#(up(x)) -> c_10(check^#(x))} {check^#(sent(x)) -> c_11(sent^#(check(x)))} ==> {sent^#(up(x)) -> c_5(sent^#(x))} {check^#(rec(x)) -> c_12(rec^#(check(x)))} ==> {rec^#(up(x)) -> c_4(rec^#(x))} {check^#(rec(x)) -> c_12(rec^#(check(x)))} ==> {rec^#(no(x)) -> c_2(sent^#(rec(x)))} {check^#(rec(x)) -> c_12(rec^#(check(x)))} ==> {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} {check^#(rec(x)) -> c_12(rec^#(check(x)))} ==> {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} {check^#(no(x)) -> c_13(no^#(check(x)))} ==> {no^#(up(x)) -> c_6(no^#(x))} {check^#(no(x)) -> c_14(no^#(x))} ==> {no^#(up(x)) -> c_6(no^#(x))} We consider the following path(s): 1) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [5] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [8] c_10(x1) = [1] x1 + [2] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} and weakly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [7] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [4] sent(x1) = [1] x1 + [5] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [13] rec^#(x1) = [1] x1 + [2] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [12] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(rec(x)) -> sent(rec(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(rec(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [2] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [14] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [4] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [3] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [6] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [9] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [10] c_0(x1) = [1] x1 + [2] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_4_0(8) -> 8 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 2) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [8] c_10(x1) = [1] x1 + [2] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(no(x)) -> c_2(sent^#(rec(x)))} and weakly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [7] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [4] sent(x1) = [1] x1 + [5] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [13] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [2] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [2] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [12] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(rec(x)) -> sent(rec(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(rec(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [2] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [14] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [3] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [6] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [9] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [15] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [2] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [8] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 2 , up_0(2) -> 2 , rec^#_0(2) -> 1 , sent^#_0(2) -> 1 , c_4_0(1) -> 1 , c_5_0(1) -> 1 , check^#_0(2) -> 1 , c_10_0(1) -> 1} 3) { top^#(rec(up(x))) -> c_7(top^#(check(rec(x)))) , top^#(no(up(x))) -> c_9(top^#(check(rec(x)))) , top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , top^#(rec(up(x))) -> c_7(top^#(check(rec(x)))) , top^#(no(up(x))) -> c_9(top^#(check(rec(x)))) , top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} Details: We apply the weight gap principle, strictly orienting the rules { rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [5] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [1] c_7(x1) = [1] x1 + [1] c_8(x1) = [1] x1 + [1] c_9(x1) = [1] x1 + [1] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [8] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [8] bot() = [3] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [1] c_7(x1) = [1] x1 + [12] c_8(x1) = [1] x1 + [8] c_9(x1) = [1] x1 + [0] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {top^#(rec(up(x))) -> c_7(top^#(check(rec(x))))} Details: Interpretation Functions: rec(x1) = [1] x1 + [4] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [2] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [1] x1 + [3] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} Weak Rules: { top^#(rec(up(x))) -> c_7(top^#(check(rec(x)))) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , top^#(sent(up(x))) -> c_8(top^#(check(rec(x))))} Weak Rules: { top^#(rec(up(x))) -> c_7(top^#(check(rec(x)))) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check(no(x)) -> no(x) , top^#(no(up(x))) -> c_9(top^#(check(rec(x))))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , top^#_0(4) -> 18 , top^#_0(5) -> 18} 4) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(no(x)) -> c_2(sent^#(rec(x)))} and weakly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [3] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [0] up(x1) = [1] x1 + [5] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [2] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [4] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 2 , up_0(2) -> 2 , rec^#_0(2) -> 1 , sent^#_0(2) -> 1 , c_4_0(1) -> 1 , check^#_0(2) -> 1 , c_10_0(1) -> 1} 5) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [8] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [4] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(no(x)) -> c_2(sent^#(rec(x)))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(no(x)) -> c_2(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [0] up(x1) = [1] x1 + [5] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [3] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [2] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 6) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} and weakly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [8] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [3] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [0] up(x1) = [1] x1 + [5] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [2] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 2 , up_0(2) -> 2 , rec^#_0(2) -> 1 , sent^#_0(2) -> 1 , c_4_0(1) -> 1 , check^#_0(2) -> 1 , c_10_0(1) -> 1} 7) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [8] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [4] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [0] up(x1) = [1] x1 + [5] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [3] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [8] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [2] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 8) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules { check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} and weakly orienting the rules { check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(rec(x)) -> sent(rec(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(rec(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [14] sent(x1) = [1] x1 + [12] no(x1) = [1] x1 + [7] bot() = [0] up(x1) = [1] x1 + [12] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [2] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [9] sent(x1) = [1] x1 + [8] no(x1) = [1] x1 + [14] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [4] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [3] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [2] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [1] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [3] c_1(x1) = [1] x1 + [4] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [7] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 9) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(up(x)) -> c_4(rec^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [8] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [6] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [8] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [1] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [14] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [1] bot() = [1] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [9] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(up(x)) -> c_4(rec^#(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(up(x)) -> c_4(rec^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [6] c_10(x1) = [1] x1 + [8] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { rec^#(up(x)) -> c_4(rec^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [1] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [3] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [7] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , c_4_0(8) -> 8 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 10) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} and weakly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [7] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [5] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [4] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules { check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [3] no(x1) = [1] x1 + [4] bot() = [1] up(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [2] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [2] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [5] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [2] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [2] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 11) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(bot()) -> c_3(sent^#(bot()))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(bot()) -> c_3(sent^#(bot()))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [1] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(bot()) -> c_3(sent^#(bot()))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(bot()) -> c_3(sent^#(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { rec^#(bot()) -> c_3(sent^#(bot())) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [1] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(bot()) -> c_3(sent^#(bot())) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [4] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [1] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [3] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(bot()) -> c_3(sent^#(bot())) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [12] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [1] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [4] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(bot()) -> c_3(sent^#(bot())) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , rec(no(x)) -> sent(rec(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(bot()) -> c_3(sent^#(bot())) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_3_0(10) -> 8 , c_4_0(8) -> 8 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 12) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {rec^#(sent(x)) -> c_1(sent^#(rec(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules { check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [8] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [8] no(x1) = [1] x1 + [10] bot() = [0] up(x1) = [1] x1 + [13] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [10] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [4] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [11] c_10(x1) = [1] x1 + [2] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [2] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [4] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [2] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [11] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x) , rec^#(sent(x)) -> c_1(sent^#(rec(x)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_4_0(8) -> 8 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 13) { check^#(up(x)) -> c_10(check^#(x)) , check^#(sent(x)) -> c_11(sent^#(check(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(sent(x)) -> c_11(sent^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(sent(x)) -> c_11(sent^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [8] c_11(x1) = [1] x1 + [6] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [1] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [1] bot() = [1] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [3] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [2] c_10(x1) = [1] x1 + [1] c_11(x1) = [1] x1 + [1] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [8] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [2] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [6] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [6] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 14) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , sent^#(up(x)) -> c_5(sent^#(x))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [1] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} and weakly orienting the rules { rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [0] up(x1) = [1] x1 + [13] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [3] c_5(x1) = [1] x1 + [2] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [5] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [2] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [1] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(up(x)) -> c_4(rec^#(x)) , check^#(up(x)) -> c_10(check^#(x)) , sent^#(up(x)) -> c_5(sent^#(x)) , rec^#(sent(x)) -> c_1(sent^#(rec(x))) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , c_4_0(8) -> 8 , c_5_0(10) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 15) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x)))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [2] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(rec(x)) -> c_12(rec^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(rec(x)) -> c_12(rec^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [15] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [14] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [7] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [1] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [8] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [5] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [3] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(no(x)) -> sent(rec(x)) , rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 16) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(rec(x)) -> c_0(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [2] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} and weakly orienting the rules { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(rec(x)) -> c_0(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [7] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [2] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [14] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [2] rec^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [1] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [2] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(rec(x)) -> c_0(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 17) { check^#(up(x)) -> c_10(check^#(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , rec^#(no(x)) -> c_2(sent^#(rec(x)))} The usable rules for this path are the following: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: We apply the weight gap principle, strictly orienting the rules { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [2] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [3] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec^#(no(x)) -> c_2(sent^#(rec(x)))} and weakly orienting the rules { check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec^#(no(x)) -> c_2(sent^#(rec(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [7] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {rec(no(x)) -> sent(rec(x))} and weakly orienting the rules { rec^#(no(x)) -> c_2(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {rec(no(x)) -> sent(rec(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [8] bot() = [0] up(x1) = [1] x1 + [2] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [5] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [14] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [2] rec^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [3] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [1] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { rec(rec(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(no(x)) -> sent(rec(x)) , rec^#(no(x)) -> c_2(sent^#(rec(x))) , check(no(x)) -> no(x) , check^#(rec(x)) -> c_12(rec^#(check(x))) , check^#(up(x)) -> c_10(check^#(x))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , rec^#_0(4) -> 8 , rec^#_0(5) -> 8 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 18) { check^#(up(x)) -> c_10(check^#(x)) , check^#(no(x)) -> c_13(no^#(check(x))) , no^#(up(x)) -> c_6(no^#(x))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(no(x)) -> c_13(no^#(check(x))) , check^#(up(x)) -> c_10(check^#(x)) , no^#(up(x)) -> c_6(no^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [4] c_6(x1) = [1] x1 + [5] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [3] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(no(x)) -> c_13(no^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(no(x)) -> c_13(no^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [2] c_6(x1) = [1] x1 + [6] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [5] c_10(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [1] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [6] sent(x1) = [1] x1 + [2] no(x1) = [1] x1 + [14] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [8] c_10(x1) = [1] x1 + [2] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { check^#(up(x)) -> c_10(check^#(x)) , no^#(up(x)) -> c_6(no^#(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { check^#(up(x)) -> c_10(check^#(x)) , no^#(up(x)) -> c_6(no^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [1] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [7] c_6(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [7] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , no^#(up(x)) -> c_6(no^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , no^#(up(x)) -> c_6(no^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , no^#_0(4) -> 16 , no^#_0(5) -> 16 , c_6_0(16) -> 16 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 19) { check^#(up(x)) -> c_10(check^#(x)) , check^#(sent(x)) -> c_11(sent^#(check(x)))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(sent(x)) -> c_11(sent^#(check(x)))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [2] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(sent(x)) -> c_11(sent^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(sent(x)) -> c_11(sent^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [7] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [10] c_10(x1) = [1] x1 + [10] c_11(x1) = [1] x1 + [1] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [14] sent(x1) = [1] x1 + [1] no(x1) = [1] x1 + [3] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [2] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [1] bot() = [0] up(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [1] x1 + [1] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [15] c_10(x1) = [1] x1 + [0] c_11(x1) = [1] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(sent(x)) -> c_11(sent^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , sent^#_0(4) -> 10 , sent^#_0(5) -> 10 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 20) { check^#(up(x)) -> c_10(check^#(x)) , check^#(no(x)) -> c_13(no^#(check(x)))} The usable rules for this path are the following: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , check(no(x)) -> no(x) , rec(rec(x)) -> sent(rec(x)) , rec(sent(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x)) , check^#(up(x)) -> c_10(check^#(x)) , check^#(no(x)) -> c_13(no^#(check(x)))} Details: We apply the weight gap principle, strictly orienting the rules {check(no(x)) -> no(x)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check(no(x)) -> no(x)} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(no(x)) -> c_13(no^#(check(x)))} and weakly orienting the rules {check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(no(x)) -> c_13(no^#(check(x)))} Details: Interpretation Functions: rec(x1) = [1] x1 + [0] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [1] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [9] c_10(x1) = [1] x1 + [15] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} and weakly orienting the rules { check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot()))} Details: Interpretation Functions: rec(x1) = [1] x1 + [15] sent(x1) = [1] x1 + [12] no(x1) = [1] x1 + [13] bot() = [2] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [9] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [0] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [1] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules { rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [1] x1 + [9] sent(x1) = [1] x1 + [0] no(x1) = [1] x1 + [0] bot() = [8] up(x1) = [1] x1 + [3] top(x1) = [0] x1 + [0] check(x1) = [1] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [13] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [1] x1 + [4] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { check(up(x)) -> up(check(x)) , check(sent(x)) -> sent(check(x)) , check(rec(x)) -> rec(check(x)) , check(no(x)) -> no(check(x)) , rec(sent(x)) -> sent(rec(x)) , rec(up(x)) -> up(rec(x)) , sent(up(x)) -> up(sent(x)) , no(up(x)) -> up(no(x))} Weak Rules: { check^#(up(x)) -> c_10(check^#(x)) , rec(rec(x)) -> sent(rec(x)) , rec(no(x)) -> sent(rec(x)) , rec(bot()) -> up(sent(bot())) , check^#(no(x)) -> c_13(no^#(check(x))) , check(no(x)) -> no(x)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { bot_0() -> 4 , up_0(4) -> 5 , up_0(5) -> 5 , no^#_0(4) -> 16 , no^#_0(5) -> 16 , check^#_0(4) -> 22 , check^#_0(5) -> 22 , c_10_0(22) -> 22} 21) { check^#(up(x)) -> c_10(check^#(x)) , check^#(no(x)) -> c_14(no^#(x)) , no^#(up(x)) -> c_6(no^#(x))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [0] x1 + [0] bot() = [0] up(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {no^#(up(x)) -> c_6(no^#(x))} Weak Rules: { check^#(no(x)) -> c_14(no^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {no^#(up(x)) -> c_6(no^#(x))} and weakly orienting the rules { check^#(no(x)) -> c_14(no^#(x)) , check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {no^#(up(x)) -> c_6(no^#(x))} Details: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [1] c_6(x1) = [1] x1 + [1] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { no^#(up(x)) -> c_6(no^#(x)) , check^#(no(x)) -> c_14(no^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: The given problem does not contain any strict rules 22) { check^#(up(x)) -> c_10(check^#(x)) , check^#(no(x)) -> c_14(no^#(x))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [0] x1 + [0] bot() = [0] up(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {check^#(no(x)) -> c_14(no^#(x))} Weak Rules: {check^#(up(x)) -> c_10(check^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {check^#(no(x)) -> c_14(no^#(x))} and weakly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(no(x)) -> c_14(no^#(x))} Details: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [1] x1 + [0] bot() = [0] up(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { check^#(no(x)) -> c_14(no^#(x)) , check^#(up(x)) -> c_10(check^#(x))} Details: The given problem does not contain any strict rules 23) {check^#(up(x)) -> c_10(check^#(x))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [0] x1 + [0] bot() = [0] up(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {check^#(up(x)) -> c_10(check^#(x))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {check^#(up(x)) -> c_10(check^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {check^#(up(x)) -> c_10(check^#(x))} Details: Interpretation Functions: rec(x1) = [0] x1 + [0] sent(x1) = [0] x1 + [0] no(x1) = [0] x1 + [0] bot() = [0] up(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] check(x1) = [0] x1 + [0] rec^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] sent^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] no^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] check^#(x1) = [1] x1 + [1] c_10(x1) = [1] x1 + [3] c_11(x1) = [0] x1 + [0] c_12(x1) = [0] x1 + [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {check^#(up(x)) -> c_10(check^#(x))} Details: The given problem does not contain any strict rules